T:Type, P:((T List)Prop), L:T List, x:T.
(L1:T List. L1  L @ [x] & P(L1)) & (L1:T List. L1  L & P(L1))

P(L @ [x]) & (L1:T List. L1  L & P(L1)) 

latex

Definitions	t  T, Prop, x(s), x:A. B(x), l1  l2, P & Q, x:A. B(x), A, as @ bs, P  Q, P  Q, P  Q, P  Q, False, ||as||, True, T, b
Lemmas	iseg weakening, iseg nil, cons iseg, squash wf, true wf, iseg append iff, append wf, not wf, iseg wf